Lower statically unreachable code to unreachable () - #232
Draft
nikswamy wants to merge 2 commits into
Draft
Conversation
An `_assert(false)` in a dead `default:` arm is a claim that control
never reaches that point, not a proposition to carry forward. PAL
emitted `assert (with_pure (0 <> 0))`, which is a proof obligation, so
the arm kept its own resource footprint and the enclosing conditional's
join came out as a `match` on the scrutinee that the frame prover could
not reduce:
- Cannot prove:
match view.version = 1ul with
| true -> ...union unfolded at the selected member...
| false -> ...union still folded...
An unreachable arm was thus the reason a proof failed.
Recognize a condition that is syntactically `0` or `false` through any
casts -- assertion bodies are C-preprocessed, so a source `false` is
already a literal by the time PAL sees it -- and emit Pulse's
`unreachable ()`. Its postcondition is `pure False`, so the arm absorbs
whatever the join needs, and the obligation becomes the right one:
prove the arm is dead, which follows from the negated branch condition.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit 09b6b9e)
It is how a noreturn abort is spelled to the C compiler, and code that ends a switch's default arm with one relies on it: without it the compiler reports the fall-through as a use of an uninitialized variable, so a function whose default arm is dead cannot be translated at all. Pulse spells the same claim 'unreachable ()', which PAL already emits for _assert(false), so a call to the builtin is rewritten to exactly that. The claim is discharged rather than assumed: an arm PAL cannot show is dead is an error, which is the point. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit a88a3cd)
Contributor
|
!diff |
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git head/builtin_unreachable/Func_halve.fst head/builtin_unreachable/Func_halve.fst
new file mode 100644
index 0000000..a2ba161
--- /dev/null
+++ head/builtin_unreachable/Func_halve.fst
@@ -0,0 +1,20 @@
+module Func_halve
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_halve (var_n: Typedef_uint32_t.ty_uint32_t)
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+ requires (with_pure (((id #int (UInt32.v var_n)) % 2) = 0))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_n = var_n;
+ if ((not
+ (((!var_n) `UInt32.rem` (id #UInt32.t (Int.Cast.int32_to_uint32 2l))) =
+ (id #UInt32.t (Int.Cast.int32_to_uint32 0l))))) {
+ unreachable ();
+ } else {};
+ return ((!var_n) `UInt32.div` (id #UInt32.t (Int.Cast.int32_to_uint32 2l)));
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_halve.fsti head/builtin_unreachable/Func_halve.fsti
new file mode 100644
index 0000000..3453e7a
--- /dev/null
+++ head/builtin_unreachable/Func_halve.fsti
@@ -0,0 +1,11 @@
+module Func_halve
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_halve (var_n: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+requires (with_pure (((id #int (UInt32.v var_n)) % 2) = 0))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/builtin_unreachable/Func_pick.fst head/builtin_unreachable/Func_pick.fst
new file mode 100644
index 0000000..f2fd7a3
--- /dev/null
+++ head/builtin_unreachable/Func_pick.fst
@@ -0,0 +1,41 @@
+module Func_pick
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_pick (var_version: Typedef_uint32_t.ty_uint32_t)
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+ requires
+ (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_version = var_version;
+ let mut var_result : Typedef_uint32_t.ty_uint32_t;
+ var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ let var___switch_scrut_0 : Typedef_uint32_t.ty_uint32_t = (!var_version);
+ let mut var___switch_hit_0 : bool;
+ var___switch_hit_0 := false;
+ let mut var___switch_brk_0 : bool;
+ var___switch_brk_0 := false;
+ if (((not (!var___switch_brk_0)) &&
+ ((!var___switch_hit_0) ||
+ (false || (var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 1l))))))) {
+ var___switch_hit_0 := true;
+ var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 10l));
+ var___switch_brk_0 := true;
+ } else {};
+ if (((not (!var___switch_brk_0)) &&
+ ((!var___switch_hit_0) ||
+ (false || (var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 2l))))))) {
+ var___switch_hit_0 := true;
+ var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 20l));
+ var___switch_brk_0 := true;
+ } else {};
+ if ((not (!var___switch_brk_0))) {
+ var___switch_hit_0 := true;
+ unreachable ();
+ } else {};
+ return (!var_result);
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_pick.fsti head/builtin_unreachable/Func_pick.fsti
new file mode 100644
index 0000000..dffbbae
--- /dev/null
+++ head/builtin_unreachable/Func_pick.fsti
@@ -0,0 +1,12 @@
+module Func_pick
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_pick (var_version: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+requires
+ (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/builtin_unreachable/TranslationErrors.fst head/builtin_unreachable/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/builtin_unreachable/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/builtin_unreachable/Typedef___uint32_t.fst head/builtin_unreachable/Typedef___uint32_t.fst
new file mode 100644
index 0000000..b9a5b44
--- /dev/null
+++ head/builtin_unreachable/Typedef___uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint32_t : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty___uint32_t__pred ([@@@mkey] this: ty___uint32_t) (p: perm) =
+ emp
+[@@pulse_eager_unfold] let predicate ty___uint32_t__uninit_pred ([@@@mkey] this: ty___uint32_t) =
+ emp
+instance has_zero_default_ty___uint32_t : (has_zero_default ty___uint32_t) =
+ { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/builtin_unreachable/Typedef_uint32_t.fst head/builtin_unreachable/Typedef_uint32_t.fst
new file mode 100644
index 0000000..aa0f488
--- /dev/null
+++ head/builtin_unreachable/Typedef_uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint32_t : Type = Typedef___uint32_t.ty___uint32_t
+[@@pulse_eager_unfold] let predicate ty_uint32_t__pred ([@@@mkey] this: ty_uint32_t) (p: perm) =
+ ((Typedef___uint32_t.ty___uint32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint32_t__uninit_pred ([@@@mkey] this: ty_uint32_t) =
+ ((Typedef___uint32_t.ty___uint32_t__uninit_pred this))
+instance has_zero_default_ty_uint32_t : (has_zero_default ty_uint32_t) =
+ { zero_default = zero_default }
\ No newline at end of file
diff --git head/builtin_unreachable/diagnostics.json head/builtin_unreachable/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/builtin_unreachable/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of the upstreaming of
nswamy/pal-c-project-integration(PR18 of 35 PRs) — seePR_PLAN.mdon that branch for the whole plan and the dependency graph.Base:
main. Depends on nothing; reviewable on its own._assert(false)in a deaddefault:arm is a claim that control never reaches there, nota proposition to carry forward; emitting
assert (with_pure (0 <> 0))left the arm's ownfootprint in the enclosing join, which then came out as an irreducible
matchon thescrutinee — making an unreachable arm the reason a proof failed. Recognizes a statically
false condition through casts and emits
unreachable (), whose postconditionpure Falseabsorbs whatever the join needs.
__builtin_unreachable— how a noreturn abort is spelledto the C compiler, and required for a dead default arm to compile at all — is rewritten to
the same thing. The claim is discharged, never assumed.
Commits
Testing
Verified:
make rust lib,test/check-template.sh,cargo fmt --check,clang-format --dry-run --Werror, and F* verification oftest/builtin_unreachable.